Inference at * 1 
Iof proof for Lemma eta conv:



1. A : Type
2. B : Type
3. f : AB
  (x.f(x)) = f 

latex

 by ((((ExtWith [] [AB]) 
CollapseTHEN (Reduce 0))) 
CollapseTHEN ((Auto_aux (first_nat 1:n
C) ((first_nat 1:n),(first_nat 3:n)) (first_tok :t) inil_term))) 

latex

C.

Definitions

x:AB(x), f(a), Type, s = t, x.A(x)